A:es_realizer{i:l}, P, Q:(ES{i}Prop{i'}).
A ||-{i} es.P(es)  (es:ES{i}. P(es)  Q(es))  A ||-{i} es.Q(es) 

latex

Definitions	R ||- es.P(es), P & Q, x:AB(x), R-Feasible(R), Consistent(R;es), x(s), f(a), x:AB(x), ES, Prop, Type, Realizer, x:A. B(x), P  Q, t  T
Lemmas	es realizer wf, event system wf, R-consistent wf, R-Feasible wf